T:Type{i}, L:(T List), R:({x:T| (x  L)} es_realizer{i:l}),
P:({x:T| (x  L)} event_system{i:l}prop{i':l}).
(x,y:T. decidable((x = y)))
 l_all(L; T; x.R-realizes{i:l}(R(x); es.P(x,es)))
 l_all(L; T; x.l_all(L; T; y.(((x = y  T))  R-compat{i:l}(R(x); R(y)))))
 R-realizes{i:l}
 R-realizes(Rall(L; x.R(x)); es.l_all(L; T; x.P(x,es))) 

latex

Definitions	guard(T), P  Q, x. t(x), t  T, x(s1,s2), x(s), l_all(L; T; x.P(x)), P  Q, prop{i:l}, x:A. B(x), decidable(P)
Lemmas	es realizer wf, decidable wf, event system wf, R-realizes wf, R-compat wf, not wf, l member wf, R-all-rule